Inference at * 1 3 1 0 
Iof proof for Lemma fincr wf:



1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. n : 
  P(n) 

latex

 by (%S% 
\p. let i = var_of_hyp (get_int_arg `hn` p) p in 
\p. let z = get_distinct_var `zz' p in

\p. Assert 
\p. (mk_all_term z  
\p. (mk_(mk_all_term i  
\p. (mk_(mk(mk_implies_term 

\p. (mk_(mk(mk_i(mk_less_than_term (mvt i) (mvt z)) 
\p. (mk_(mk(mk(concl p)))) 
\p. p) 

latex

\p1: .....assertion..... NILNIL

\p1:   zz, n:. (n < zz)  (P(n))
\p2: 

\p2: 4. zz, n:. (n < zz)  (P(n))
\p2:   P(n)
\p.

Definitions

f(a), a < b, P  Q, x:A. B(x), , , x:AB(x)